Rewrite the Ranking Protocol as the DRanking paper - #698

8c36d7d recasts the paper in the rings.tex formal register per author direction: minimal prose, maximal math. Definitions/assumptions/laws are now symbol arrays; added proved content beyond the prose version — mass invariant, statistical-undetectability proposition (position tests have zero advantage against uniform Sybil placement), grinding closure, Chernoff committee-safety bound, epoch transition as pseudocode with cost, linearity-of-IVC proof via quorum intersection, payable-rank market-clearing derivation, and PoW/PoT rejection as a formal constraint. 5 pages, zero overfull boxes, zero bibtex warnings.

c105f9c extends the paper with new formal content: a farming-price proposition (single-node instance of the Sybil bound, making the farm() function of the payable-rank argument explicit), an l1-contraction convergence proof for the unrolled fixpoint, unification of the time-varying damping schedule with all propositions, a threshold-authority definition closing the seed-compromise threat row, a TLA-style State Relation section (Spec/Init/Next + slash-monotone, version-monotone, unique-chain invariants, with a finite-instance model-checking obligation), a balance-conservation invariant, formalized commitment granularity (full/agg/blind leakage profiles) replacing the prose privacy remark, and an epoch-cycle dataflow figure. Also fixes two notation collisions (random-oracle h vs honest region H; Vrfy vs node set V) and corrects the linearity proof to cite the per-phase quorum assumption. Still 5 pages, zero overfull boxes, zero bibtex warnings.

1152622 hardens the protocol content. The substantive fix: the previous beacon (hash of the finalized header) was grindable — a proposer can steer the next epoch's sortition by selecting what to include in the block. Replaced with a unique threshold-signature beacon B_k = h(TSig_S(k)); BLS uniqueness leaves no free variable to grind, stated as an unbiasability proposition and wired into the grinding-closure proof. Also added: a fixed-point arithmetization definition with a rounding-soundness proposition (floor rounding never overcounts weight, and the l1 contraction damps accumulated error to n·2^-phi/(1-alpha) for all time); weak fairness in the TLA spec plus a progress proposition under partial synchrony; a countersigning-game proposition (truthful receipt issuance weakly dominant under tit-for-tat; receipt sale is attack-edge formation, priced and capped); and a nine-parameter table with constraints and back-references. 6 pages, zero overfull, zero bibtex warnings.

efdad15 fixes the CI failure: the typos gate flagged author surnames in papers/dranking.bib (Brin from the PageRank citation, Pease from the Byzantine Generals citation) as misspellings. Added both as extend-words in typos.toml — scoped to the word list, so code spell-checking is not loosened. Verified locally with a clean full-repo typos run; all other checks on the PR were already green.

1edf7c1 (merged as b58390c with master) closes the implementability and completeness gaps from self-review. Soundness fixes — two invariant proofs did not hold as previously stated: (1) slashing now cuts the trust vector, both matrix dimensions, AND the seed vector — restricting the vector alone let receipts naming a slashed server, or a fixed seed share, re-grant mass one epoch later (Law 3, Algorithm 2, and the slash-monotone proof restructured; a slashed seed's share burns); (2) sortition is atomized Algorand-style (inverse-binomial seats over fixed-point weight atoms), removing two hidden hypotheses of indicator sortition — the per-node cap tau·t(v) ≤ 1 (violated by seeds at cold start) and total-mass normalization (violated once slashes burn mass); (3) the epoch transition is retyped as F(Sigma, X_k) with rt(X_k) public input and the block as witness — the old signature F(Sigma, rt(W)) did not provide the receipts, proofs, and fees its own body consumed. Structural completions: canonical input-block aggregation with per-epoch dedup; inductive beacon group with gpk-preserving proactive resharing (resolves the staked-phase circularity where TSig was bound to the retired seed set); per-proposer attributable force inclusion; transfer/bond/unbond semantics for the reward asset; a verification-boundary obligation (EC verifications out-of-fold, QC-attested, fraud-proof-backed); and a carrier-boundedness proposition (fixed-point truncation is free GC, |carrier| ≤ 2^phi). 7 pages, zero overfull, zero bibtex warnings.